Nuprl Definition : set_prod
13,42
postcript
pdf
s
t
== mk_dset(
:|
s
|
|
t
|,
a
,
b
.
a
=
b
)
latex
clarification:
s
t
== mk_dset(
:|
s
|
|
t
|,
a
,
b
.
a
=
s
,
t
b
)
latex
Up
sets
1
Wellformedness Lemmas
set
prod
wf
Definitions
mk_dset(
T
,
eq
)
,
|
p
|
,
a
=
b
origin
t == mk_dset(:|s| |t|, 
a,b. a =
b)
t == mk_dset(:|s| |t|, a,b. a =s,t b) t == mk_dset(:|s| |t|, a,b. a = b)
t == mk_dset(:|s| |t|, a,b. a =s,t b) b